n:, a:. sum(a | x < n) = (a * n) 

latex

Definitions	False, A, A  B, i  j , , P  Q, ff, tt, (i = j), if b then t else f fi , Y, t  T, primrec(n;b;c), sum(f(x) | x < k), x:A. B(x), , P & Q, P  Q, Unit, ,
Lemmas	ge wf, nat properties, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, assert of eq int, eqtt to assert, assert wf, iff transitivity, bool wf, eq int wf, nat wf